k:Knd. (isrcv(k))  (k = rcv(lnk(k),tag(k))) 

latex

Definitions	x:A. B(x), P  Q, b, isrcv(k), rcv(l,tg), lnk(k), tag(k), isl(x), t.1, outl(x), t.2, tt, ff, if b then t else f fi , t  T, Knd, False, prop{i:l}
Lemmas	rcv wf, true wf, false wf, assert wf, isrcv wf, Knd wf